Nuprl Definition : es-dt 11,40

es-dt(l; da)
== compose-fpf((k.if isrcv(k)
== compose-fpf(then if eq_lnk(lnk(k); l) then inl tag(k)  else inr   fi 
== compose-fpf(else inr  
== compose-fpf(fi );
== compose-fpf((tg.rcv(l,tg));
== compose-fpf(da) 
latex


Definitionscompose-fpf(a; b; f), isrcv(k), if b then t else f fi , eq_lnk(a; b), lnk(k), inl x , tag(k), inr x , , x.A(x), rcv(l,tg)
FDL editor aliaseses-dt

origin